Step of Proof: bool-to-neg-dcdr-aux
11,40
postcript
pdf
Inference at
*
I
of proof for Lemma
bool-to-neg-dcdr-aux
:
A
:Type,
f
:(
A
),
x
:
A
. Dec(
f
(
x
) = ff)
latex
by Auto
latex
.
Definitions
Dec(
P
)
,
s
=
t
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
ff
,
x
:
A
B
(
x
)
,
,
t
T
,
Type
Lemmas
decidable
equal
bool
,
bfalse
wf
,
bool
wf
origin
A:Type, f:(A
), x:A. Dec(f(x) = ff)
by Auto
. A:Type, f:(A), x:A. Dec(f(x) = ff)
by Auto
.x:A. B(x)B(x)
T